COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	know.lsp[f83,jmc]	EKL axioms for knowledge
C00004 ENDMK
C⊗;
know.lsp[f83,jmc]	EKL axioms for knowledge
(decl true1 |ground → truthval| (syntype: constant))
(decl true |ground⊗ground → truthval| (syntype: constant))

(decl (white black) |ground| (syntype: constant))

(axiom |white ≠ black|)

(decl iscolor |ground→truthval| (syntype: constant) (unaryname: iscolor)
	(bindingpower: 850))

(axiom |∀c.iscolor c ≡ c = white ∨ c = black|)

(axiom |∀c1 c2 c3.iscolor c1 ∧ iscolor c2 ∧ iscolor c3
	⊃ ∃state.(color(per1,state) = c1 ∧ color(per2,state) = c2
		∧ color(per3,state) = c3)|)

0*(¬S1*¬(p1∧p2∧p3)
∧¬S1*(p1∧p2∧¬p3)
∧¬S1*(p1∧¬p2∧p3)
∧¬S1*(p1∧¬p2∧¬p3)
∧¬S1*(¬p1∧p2∧p3)
∧¬S1*(¬p1∧p2∧¬p3)
∧¬S1*(¬p1∧¬p2∧p3)
∧¬S1*(¬p1∧¬p2∧¬p3)
∧¬S2*(p1∧p2∧p3)
∧¬S2*(p1∧p2∧¬p3)
∧¬S2*(p1∧¬p2∧p3)
∧¬S2*(p1∧¬p2∧¬p3)
∧¬S2*(¬p1∧p2∧p3)
∧¬S2*(¬p1∧p2∧¬p3)
∧¬S2*(¬p1∧¬p2∧p3)
∧¬S2*(¬p1∧¬p2∧¬p3)
∧¬S3*(p1∧p2∧p3)
∧¬S3*(p1∧p2∧¬p3)
∧¬S3*(p1∧¬p2∧p3)
∧¬S3*(p1∧¬p2∧¬p3)
∧¬S3*(¬p1∧p2∧p3)
∧¬S3*(¬p1∧p2∧¬p3)
∧¬S3*(¬p1∧¬p2∧p3)
∧¬S3*(¬p1∧¬p2∧¬p3))